(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun v0 () (Array Index Element))
(declare-fun v1 () Index)
(declare-fun v2 () Index)
(declare-fun v3 () Element)
(declare-fun v4 () Element)
(declare-fun v5 () Element)
(declare-fun v6 () Element)
(declare-fun v7 () Element)
(check-sat-assuming ( (let ((_let_0 (store v0 v2 v7))) (let ((_let_1 (= v0 _let_0))) (let ((_let_2 (distinct v2 v1))) (let ((_let_3 (= v6 v4))) (let ((_let_4 (= v6 v7))) (let ((_let_5 (= v5 v6))) (let ((_let_6 (ite _let_1 v0 _let_0))) (let ((_let_7 (ite _let_1 v0 (ite _let_2 (ite (distinct v4 v3) v0 v0) v0)))) (let ((_let_8 (ite (distinct v4 v3) (ite _let_2 (ite (distinct v4 v3) v0 v0) v0) (ite _let_2 (ite (distinct v4 v3) v0 v0) v0)))) (let ((_let_9 (ite _let_5 (ite (distinct v6 (select _let_0 v1)) _let_7 (ite (distinct v4 v4) _let_7 _let_6)) (ite (distinct v4 v4) _let_7 _let_6)))) (let ((_let_10 (ite _let_1 v1 v1))) (let ((_let_11 (ite (distinct v6 (select _let_0 v1)) v2 v1))) (let ((_let_12 (ite (distinct v4 v4) v1 v2))) (let ((_let_13 (ite _let_2 (ite _let_2 _let_12 (ite _let_3 _let_10 (ite _let_5 v2 v1))) v1))) (let ((_let_14 (ite (distinct v4 v3) v1 _let_13))) (let ((_let_15 (ite (distinct v4 v4) v4 v6))) (let ((_let_16 (ite (distinct v4 v3) v5 v6))) (let ((_let_17 (ite _let_2 v5 v7))) (let ((_let_18 (ite _let_1 _let_16 _let_17))) (let ((_let_19 (ite _let_3 v4 _let_18))) (let ((_let_20 (ite _let_5 _let_15 v4))) (let ((_let_21 (store _let_0 _let_14 v7))) (let ((_let_22 (or (distinct v4 v3) (xor (distinct (ite (distinct v6 (select _let_0 v1)) _let_7 (ite (distinct v4 v4) _let_7 _let_6)) (ite (distinct v6 (select _let_0 v1)) _let_7 (ite (distinct v4 v4) _let_7 _let_6))) (= (ite (distinct v4 v3) (ite _let_3 _let_6 (ite (distinct v4 v3) v0 v0)) (ite _let_2 (ite (distinct v4 v3) v0 v0) v0)) _let_0))))) (let ((_let_23 (and (not (distinct (ite _let_3 _let_10 (ite _let_5 v2 v1)) (ite _let_3 _let_10 (ite _let_5 v2 v1)))) (or (= (distinct _let_6 _let_0) (= (ite _let_3 _let_10 (ite _let_5 v2 v1)) (ite _let_3 _let_10 (ite _let_5 v2 v1)))) (ite (=> (= v6 v3) (distinct v7 v4)) (or (= (ite (= _let_6 _let_21) _let_4 (ite (= _let_9 _let_7) (distinct (ite _let_4 (ite (distinct v4 v4) _let_7 _let_6) _let_7) (ite (distinct v4 v3) v0 v0)) (distinct v0 (ite (distinct v4 v4) _let_7 _let_6)))) (= v4 (ite _let_4 (select _let_0 v1) v3))) (distinct _let_16 v6)) (distinct v3 _let_19)))))) (let ((_let_24 (= (= (not (= (ite (distinct v4 v3) v0 v0) (ite (distinct v4 v3) (ite _let_3 _let_6 (ite (distinct v4 v3) v0 v0)) (ite _let_2 (ite (distinct v4 v3) v0 v0) v0)))) (distinct (ite _let_2 _let_12 (ite _let_3 _let_10 (ite _let_5 v2 v1))) _let_12)) (=> (and (and (not (distinct (ite (distinct v4 v3) v0 v0) (ite (distinct v4 v4) _let_7 _let_6))) (not (distinct (ite (distinct v4 v3) v0 v0) (ite (distinct v4 v4) _let_7 _let_6)))) (and (distinct _let_13 v2) (and (xor (distinct _let_11 v1) (not (ite (= (xor (= (distinct (ite _let_3 _let_6 (ite (distinct v4 v3) v0 v0)) _let_8) (= _let_2 (= _let_0 (ite (distinct v4 v4) _let_7 _let_6)))) _let_5) (distinct _let_10 (ite _let_3 _let_10 (ite _let_5 v2 v1)))) _let_3 (distinct _let_12 (ite _let_4 (ite _let_5 v2 v1) _let_11))))) (ite (distinct _let_9 (ite _let_3 _let_6 (ite (distinct v4 v3) v0 v0))) (distinct (ite _let_5 v2 v1) _let_10) (distinct _let_21 v0))))) (and (distinct _let_21 _let_6) (= (or (distinct _let_14 v2) (=> (distinct (ite (distinct v4 v4) _let_7 _let_6) _let_9) (distinct v4 (select _let_6 _let_12)))) (ite (distinct (ite (distinct v6 (select _let_0 v1)) _let_16 v3) (ite _let_4 (select _let_0 v1) v3)) (= _let_18 (select _let_0 v1)) (distinct v2 _let_12)))))))) (=> (= _let_24 _let_24) (= (=> (and (ite _let_23 (= (=> (xor (distinct _let_10 (ite _let_2 _let_12 (ite _let_3 _let_10 (ite _let_5 v2 v1)))) (= _let_20 v3)) (distinct (ite _let_2 (ite (distinct v4 v3) v0 v0) v0) _let_8)) (and (distinct _let_17 v6) (distinct (ite (distinct v6 (select _let_0 v1)) _let_7 (ite (distinct v4 v4) _let_7 _let_6)) _let_8))) _let_23) (and (and (distinct v4 (select _let_0 v1)) (distinct v4 v4)) (= (or (or (= (ite _let_2 _let_12 (ite _let_3 _let_10 (ite _let_5 v2 v1))) (ite _let_2 _let_12 (ite _let_3 _let_10 (ite _let_5 v2 v1)))) (distinct _let_18 v4)) (and (= v7 _let_20) (distinct _let_16 v5))) (and (= (ite (distinct v6 (select _let_0 v1)) _let_7 (ite (distinct v4 v4) _let_7 _let_6)) _let_6) (= (= (ite (distinct _let_18 v7) (= (distinct _let_7 (ite (distinct v4 v4) _let_7 _let_6)) (= _let_6 _let_6)) (=> (not (distinct (select _let_0 v1) _let_20)) (distinct v6 (select _let_0 v1)))) (not (= _let_8 _let_21))) (=> (distinct _let_14 _let_10) (distinct _let_9 _let_7))))))) (and (= (or (or (distinct _let_0 (ite (distinct v4 v3) v0 v0)) (xor (= _let_16 _let_20) _let_1)) (xor (distinct (ite _let_3 _let_6 (ite (distinct v4 v3) v0 v0)) v0) (ite (= v4 _let_17) (distinct v6 v4) (distinct _let_15 v3)))) (not (distinct _let_19 _let_16))) (= (xor (distinct _let_9 _let_6) (or _let_22 _let_22)) (not (not (distinct (ite (distinct v4 v3) v0 v0) _let_8)))))) (distinct _let_13 _let_12)))))))))))))))))))))))))))) ))
